es:ES, e:E, l:IdLnk, tg:Id. (e sends on l with tag tg)  (es-first-from(es;e;l;tg)  E) 

latex

Definitions

Top, null(as), t.2, if b then t else f fi , tt, tag(k), b, outl(x), t.1, SQType(T), {T}, lnk(k), rcv(l,tg), Y, ||as||, True, T, xL. P(x), x. t(x), , P & Q, A c B, es-first-from(es;e;l;tg), t  T, P  Q, IdLnk, x:A. B(x), False, A, P  Q, x:A. B(x), (e sends on l with tag tg), SqStable(P), P  Q, x(s), lnk(e), isrcv(e)

Lemmas

top wf, null wf3, filter wf, member null, l member set, assert-eq-id, Knd wf, Knd sq, es-kind-rcv, member filter, non neg length, length wf1, subtype rel list, hd wf, decidable assert, isrcv wf, sq stable from decidable, tagof wf, eq id wf, es-kind wf, es-isrcv wf, assert wf, filter type, l member wf, member-es-receives, es-receives wf, list-set-type2, event system wf, es-E wf, IdLnk wf, Id wf, es-sends-on wf, es-sender wf, lnk wf